﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Threading.Tasks;
using System.Numerics;

namespace OverSATbLib
{
    public class SatSolver
    {

        class Variable
        {
            public int Name;
            public int ColumnIndex;
            public BigInteger AssignMask;
        }

        class Clause
        {
            public List<int> VariableReferences = new List<int>();
            public uint NotBits;
            public uint NotBitMask;

            public Tuple CreateTuple(uint localBits)
            {
                Tuple t = new Tuple();
                uint bitIndex = 1;
                int count = 0;
                while (count < VariableReferences.Count)
                {
                    var c = VariableReferences[count];
                    t.AssignItems.Add(new Assignment
                    {
                        NameId = c,
                        Value = ((localBits & bitIndex) > 0) ? 1u : 0
                    });
                    bitIndex <<= 1;
                    count++;
                }
                return t;
            }

            /// <summary>
            /// Test returns true if the local bits given actually evaluate to true in a SAT clause
            /// </summary>
            /// <param name="localBits"></param>
            /// <returns></returns>
            public bool TestOrClause(uint localBits)
            {
                uint BitsThatAreNotted = localBits & NotBits;
                uint NottedValues = BitsThatAreNotted ^ NotBits;
                uint OtherValues = localBits & NotBitMask;
                return (NottedValues > 0 || OtherValues > 0);
            }
        }

        List<Clause> Clauses = new List<Clause>();
        List<Variable> Variables = new List<Variable>();
        Dictionary<int, Variable> VariablesById = new Dictionary<int, Variable>();
        private int CurrentColumnIndex = 0;

        public BigInteger TotalRows = 0;
        public List<Tuple> DeletedTuples = new List<Tuple>();

        public List<int> VariablesUsed { get { return Variables.Select(a => a.Name).Distinct().ToList(); } }

        public int ClausesUsed { get { return Clauses.Count; } }

        public uint GetValue(int nameId, BigInteger rowIdx)
        {
            Variable v = VariablesById[nameId];
            uint vn = (v.AssignMask & rowIdx) > 0 ? 1u : 0u;
            return vn;
        }

        public Range GetNextMatchingRange(int nameId, BigInteger searchRowIdx, uint searchValue)
        {
            Range result = new Range();

            Variable v = VariablesById[nameId];

            uint value = (v.AssignMask & searchRowIdx) > 0 ? 1u : 0u;
            BigInteger band = v.AssignMask * 2;

            if (value == searchValue)
            {
                result.Start = searchRowIdx;
                result.Stop = result.Start + (v.AssignMask - result.Start % v.AssignMask);
                result.Empty = false;
            }
            else if (value < searchValue)
            {
                BigInteger delta = (searchValue - value) * v.AssignMask;
                result.Start = (searchRowIdx / v.AssignMask) * v.AssignMask + delta;
                result.Stop = result.Start + (v.AssignMask - result.Start % v.AssignMask);
                result.Empty = false;
            }
            else
            {
                result.Start = (((searchRowIdx / band) + 1) * band) + (searchValue * v.AssignMask);
                result.Stop = result.Start + (v.AssignMask - result.Start % v.AssignMask);
                result.Empty = false;
            }

            return result;
        }

        public BigInteger CountBitRows(int nameId, uint value, Range r)
        {
            var assign = new Assignment
            {
                Index = VariablesById[nameId].ColumnIndex,
                Value = value,
                NameId = nameId
            };

            return CountBitRows(assign, r);
        }

        /// <summary>
        /// This is the basis of the new approach
        /// foreach tuple in deletes
        ///     countrows range
        ///     foreach tuple2 in deletes
        ///         intersect = intersect tuple1, tuple2
        /// </summary>
        /// <param name="t"></param>
        /// <param name="r"></param>
        /// <returns></returns>
        public BigInteger CountBitRows( Assignment assign, Range r )
        {
            BigInteger  total = 0;
            BigInteger mark, m, t;
            BigInteger size = 1;

            Range workingRange = new Range
            {
                Start = r.Start,
                Stop = r.Stop,
                Empty = false
            };

            size <<= assign.Index;

            m = (workingRange.Start % size);
            if (m > 0)
            {
                mark = ((workingRange.Start + size) / size * size);

                if (mark > workingRange.Stop)
                {
                    mark = workingRange.Stop;
                }

                if (GetValue(assign.NameId, workingRange.Start) == assign.Value)
                {
                    total += (mark - workingRange.Start);
                }

                workingRange.Start = mark;
            }

            mark = workingRange.Stop / size * size;
            m = mark - workingRange.Start;

            if (m >= 0)
            {
                if (m > size)
                {
                    t = m / 2;
                    total += t;
                }
                else if (GetValue(assign.NameId, workingRange.Start) == assign.Value)
                {
                    total += (mark - workingRange.Start);
                }

                workingRange.Start = mark;

                if (GetValue(assign.NameId, workingRange.Start) == assign.Value)
                {
                    total += (workingRange.Stop - workingRange.Start);
                }
            }

            return total;
        }

        public BigInteger CountRowsBruteForce(Tuple t, Range range)
        {
            BigInteger count = 0;
            BigInteger bi = 0;
            for (bi = range.Start; bi < range.Stop; bi++)
            {
                if (Test(bi, t))
                {
                    count++;
                }
            }
            return count;
        }

        public BigInteger CountRows( Tuple t, Range range )
        {
            BigInteger baseRows = range.Size;

            int assignIndex = 0;

            while (baseRows == range.Size && assignIndex < t.AssignItems.Count)
            {
                var firstAssign = t.AssignItems[assignIndex];
                baseRows = CountBitRows(firstAssign, range);
                assignIndex++;
            }

            for (int i = assignIndex; i < t.AssignItems.Count; i++)
            {
                baseRows = baseRows / 2;
            }

            return baseRows;
        }

        public void AddClause(IEnumerable<int> cnfStyleVariables)
        {
            int k = cnfStyleVariables.Count();
            if (k == 0)
                return;

            if (k > 32)
                throw new ClauseHasTooManyVariablesException(cnfStyleVariables);

            var dups = cnfStyleVariables
                .Select(a => Math.Abs(a))
                .GroupBy(a => a)
                .Where(a => a.Count() > 1)
                .Count();

            if (dups > 0)
                throw new ClauseHasDuplicateVariablesExeption(cnfStyleVariables);

            Clause c = new Clause();

            uint clauseBitIndex = 1;

            foreach (var n in cnfStyleVariables)
            {
                int nameId;
                if (n < 0)
                {
                    c.NotBits |= clauseBitIndex;
                    nameId = -n;
                }
                else
                {
                    nameId = n;
                }
                c.VariableReferences.Add(nameId);
                clauseBitIndex <<= 1;
                if (!VariablesById.ContainsKey(nameId))
                {
                    BigInteger mask = new BigInteger(1);
                    mask <<= CurrentColumnIndex;
                    Variable v = new Variable
                    {
                        ColumnIndex = CurrentColumnIndex,
                        Name = nameId,
                        AssignMask = mask
                    };
                    Variables.Add(v);
                    VariablesById.Add(nameId, v);
                    if (TotalRows == BigInteger.Zero)
                    {
                        TotalRows = 2;
                    }
                    else
                    {
                        TotalRows *= 2;
                    }
                    CurrentColumnIndex++;
                }
            }

            c.NotBitMask = ~c.NotBits;

            // now, generate deletes

            for (uint bt = 0; bt < clauseBitIndex; bt++)
            {
                var t = c.TestOrClause(bt);
                if (!t)
                {
                    var delTuple = c.CreateTuple(bt);
                    DeleteTuple(delTuple);
                }
            }

            Clauses.Add(c);
        }

        public void Optimize()
        {
            TupleSet ts = new TupleSet();
            ts.Solver = this;
            ts.Tuples.AddRange(DeletedTuples);
            ts.Normalize();
            DeletedTuples = ts.Tuples;
        }

        private uint MapClauseBits(BigInteger index, Clause c)
        {
            uint bits = 0;
            int bitShift = 0;
            for (int i = 0; i < c.VariableReferences.Count; i++)
            {
                int cv = c.VariableReferences[i];
                var b = GetValue(c.VariableReferences[i], index);
                b <<= bitShift;
                bits |= b;
                bitShift++;
            }
            return bits;
        }

        private bool Test(BigInteger index, Clause c)
        {
            uint bits = MapClauseBits(index, c);
            bool result = c.TestOrClause(bits);
            return result;
        }

        public bool Test( BigInteger index, Tuple t )
        {
            foreach (var a in t.AssignItems)
            {
                var v = Variables[a.Index];
                int val = (index & v.AssignMask) > 0 ? 1 : 0;
                if (val != a.Value)
                    return false;
            }
            return true;
        }

        public bool Test(BigInteger index)
        {
            foreach (var c in Clauses)
            {
                if (!Test(index, c))
                {
                    return false;
                }
            }
            return true;
        }

        public void RegisterTuple( Tuple t )
        {
            foreach (var a in t.AssignItems)
            {
                var c = this.VariablesById[a.NameId];
                a.Index = c.ColumnIndex;
            }
            t.AssignItems.Sort((a, b) => { return b.Index - a.Index; });
        }

        public void DeleteTuple( Tuple t )
        {
            RegisterTuple(t);
            DeletedTuples.Add(t);
        }

        public Tuple GetValueAtRow(BigInteger rowIdx)
        {
            Tuple t = new Tuple();

            foreach (var col in Variables)
            {
                var assign = new Assignment();
                assign.NameId = col.Name;
                assign.Value = GetValue(assign.NameId, rowIdx);
                t.AssignItems.Add(assign);
            }

            return t;
        }

        public class TestRangeRequest
        {
            public Range Range;
            public List<Tuple> DeletedTuples;
        }

        public class TestRangeResponse
        {
            public bool HasTrues;
            public Range Range;
            public List<Tuple> NewDeletedTuples;
        }

        public TestRangeResponse TestRange(TestRangeRequest request)
        {
            Range range = request.Range;
            List<Tuple> checkTuples = request.DeletedTuples;

            TestRangeResponse response = new TestRangeResponse
            {
                HasTrues = false,
                Range = range,
                NewDeletedTuples = new List<Tuple>()
            };

            List<Tuple> bucket = response.NewDeletedTuples;
            List<Tuple> intersections = new List<Tuple>();

            BigInteger total = 0;
            BigInteger span = (range.Stop - range.Start);

            if (request.Range.Size == 0)
            {
                response.HasTrues = false;
                return response;
            }

            for (int i = 0; i < checkTuples.Count; i++)
            {
                var outerDel = checkTuples[i];
                BigInteger outerCount = CountRows(outerDel, range);

                total += outerCount;

                if (total >= span)
                {
                    response.HasTrues = false;
                    return response;
                }
            }

            response.HasTrues = true;

            return response;
        }

        public bool FindTrueValue( List<Tuple> deletedTuples, List<Tuple> trueValues, int topValues, Range range, int depth )
        {
            if (trueValues.Count >= topValues)
                return true;

            var width = ( range.Stop - range.Start );

            var response = TestRange(new TestRangeRequest
            {
                Range = range,
                DeletedTuples = deletedTuples
            });

            if (response.HasTrues)
            {
                if (range.Size > 1)
                {
                    Console.WriteLine("dive,{0},{1}-{2}", depth, range.Start, range.Stop);
                    System.Diagnostics.Debug.WriteLine("dive,{0},{1}-{2}", depth, range.Start, range.Stop);
                    Range first = new Range();
                    Range second = new Range();
                    first.Start = range.Start;
                    first.Stop = range.Size / 2 + range.Start;
                    second.Start = first.Stop;
                    second.Stop = range.Stop;
                    depth++;
                    bool retA, retB;
                    retA = FindTrueValue(response.NewDeletedTuples, trueValues, topValues, first, depth);
                    retB = FindTrueValue(response.NewDeletedTuples, trueValues, topValues, second, depth);
                    if (!(retA || retB))
                    {
                        Console.WriteLine("epic fail,{0},{1}-{2}", depth, range.Start, range.Stop);
                        System.Diagnostics.Debug.WriteLine("epic fail,{0},{1}-{2}", depth, range.Start, range.Stop);
                        //throw new Exception("Expecting range to be true and it wasn't.");
                    }
                    return true;
                }
                else if (Test(range.Start))
                {
                    Console.WriteLine("found,{0},{1}-{2}", depth, range.Start, range.Stop);
                    System.Diagnostics.Debug.WriteLine("found,{0},{1}-{2}", depth, range.Start, range.Stop);
                    Tuple t = GetValueAtRow(range.Start);
                    trueValues.Add(t);
                    return true;
                }
                else
                {
                    Console.WriteLine("fail,{0},{1}-{2}", depth, range.Start, range.Stop);
                    System.Diagnostics.Debug.WriteLine("fail,{0},{1}-{2}", depth, range.Start, range.Stop);
                    throw new Exception("Expecting range to be true and it wasn't.");
                    return false;
                }
            }
            else
            {
                Console.WriteLine("nope,{0},{1}-{2}", depth, range.Start, range.Stop);
                System.Diagnostics.Debug.WriteLine("nope,{0},{1}-{2}", depth, range.Start, range.Stop);
                return false;
            }
        }

        public List<Tuple> GetTrueValues(int topValues)
        {
            Optimize();
            List<Tuple> foundTuples = new List<Tuple>();
            Range r = new Range();
            r.Start = 0;
            r.Stop = TotalRows;
            FindTrueValue(DeletedTuples, foundTuples, topValues, r, 0);
            return foundTuples;
        }

        public List<Tuple> GetTrueValuesBruteForce(int topValues)
        {
            List<Tuple> tuples = new List<Tuple>();
            BigInteger row = 0;
            int c = 0;
            while (row < this.TotalRows && c < topValues)
            {
                if (Test(row))
                {
                    Tuple t = GetValueAtRow(row);
                    tuples.Add(t);
                }
                row++;
                c++;
            }
            return tuples;
        }

        public static void Test()
        {
            SatSolver solver = new SatSolver();

            solver.AddClause(new int[] { -1, 2, 3 });
            List<Tuple> tuples = solver.GetTrueValues(5);
            foreach (var t in tuples)
            {
                Console.WriteLine(t.ToString());
            }
        }

    }

    public class IdPair
    {
        public int Id0 { get; set; }
        public int Id1 { get; set; }

        public override bool Equals(object obj)
        {
            var o = obj as IdPair;
            return o.Id0 == Id0 && o.Id1 == Id1;
        }

        public override int GetHashCode()
        {
            return Id0 ^ Id1;
        }
    }


}
